Nuprl Lemma : f2f+-p+_wf
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
f2f+
:F2F+-decls,
sndr
,
rcvr
:
ff
.C. f2f+-p+
E
E
latex
Definitions
P
Q
,
P
&
Q
,
f2f+-p+
,
,
t
T
,
F2F+-decls
,
FIFO
,
x
:
A
.
B
(
x
)
Lemmas
event
system
wf
,
fifo
wf
,
es-state
wf
,
es-E
wf
,
bool
wf
,
es-dtype
wf
,
fifoR
wf
,
decidable
wf
,
es-loc
wf
,
Id
wf
,
fifoS
wf
,
snd-it
wf
,
not
wf
,
fifoC
wf
,
top
wf
,
f2f+-pred
wf
,
rel
plus
wf
origin
es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C. f2f+-p+ 
E
E
es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C. f2f+-p+ EE 
Q Tx:A. B(x)